es:ES, e', e, a:E. (e <loc a) & a  e'   [e, e'] = ([e, pred(a)] @ [a, e'])  E List 

latex

Definitions	x:A. B(x), P  Q, P & Q, t  T, Prop, x. t(x), P  Q, P  Q, T, True, WellFnd{i}(A;x,y.R(x;y)), x(s), {T}, P  Q, A & B
Lemmas	es-locl-wellfnd, es-E wf, es-locl wf, es-le wf, es-interval wf, append wf, es-pred wf, es-locl-iff, es-interval-less, es-le-trans3, event system wf, es-le-iff, es-pred-locl, append assoc, squash wf, true wf, es-le-pred, not wf, assert wf, es-first wf, es-interval-eq